0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 94 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 22 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 3 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 UsableRulesReductionPairsProof (⇔, 104 ms)
↳22 QDP
↳23 DependencyGraphProof (⇔, 0 ms)
↳24 QDP
↳25 UsableRulesProof (⇔, 0 ms)
↳26 QDP
↳27 QReductionProof (⇔, 0 ms)
↳28 QDP
↳29 QDPSizeChangeProof (⇔, 0 ms)
↳30 YES
sameleavesC_in_gg(leaf(T6), leaf(T6)) → sameleavesC_out_gg(leaf(T6), leaf(T6))
sameleavesC_in_gg(tree(T11, T12), tree(T13, T14)) → U6_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_in_ggga(T13, T14, T23, X17))
getleaveA_in_ggga(leaf(T42), T43, T42, T43) → getleaveA_out_ggga(leaf(T42), T43, T42, T43)
getleaveA_in_ggga(tree(T52, T53), T54, T55, X63) → U1_ggga(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
U1_ggga(T52, T53, T54, T55, X63, getleaveA_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveA_out_ggga(tree(T52, T53), T54, T55, X63)
U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_out_ggga(T13, T14, T23, X17)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_in_gg(T24, T29))
U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_out_gg(T24, T29)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U6_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesC_out_gg(tree(T11, T12), tree(T13, T14))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
sameleavesC_in_gg(leaf(T6), leaf(T6)) → sameleavesC_out_gg(leaf(T6), leaf(T6))
sameleavesC_in_gg(tree(T11, T12), tree(T13, T14)) → U6_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_in_ggga(T13, T14, T23, X17))
getleaveA_in_ggga(leaf(T42), T43, T42, T43) → getleaveA_out_ggga(leaf(T42), T43, T42, T43)
getleaveA_in_ggga(tree(T52, T53), T54, T55, X63) → U1_ggga(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
U1_ggga(T52, T53, T54, T55, X63, getleaveA_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveA_out_ggga(tree(T52, T53), T54, T55, X63)
U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_out_ggga(T13, T14, T23, X17)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_in_gg(T24, T29))
U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_out_gg(T24, T29)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U6_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesC_out_gg(tree(T11, T12), tree(T13, T14))
SAMELEAVESC_IN_GG(tree(T11, T12), tree(T13, T14)) → U6_GG(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
SAMELEAVESC_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, X15, X16, T13, T14, X17)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → U2_GGAAGGA(T23, T24, T13, T14, X17, getleaveA_in_ggga(T13, T14, T23, X17))
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → GETLEAVEA_IN_GGGA(T13, T14, T23, X17)
GETLEAVEA_IN_GGGA(tree(T52, T53), T54, T55, X63) → U1_GGGA(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
GETLEAVEA_IN_GGGA(tree(T52, T53), T54, T55, X63) → GETLEAVEA_IN_GGGA(T52, tree(T53, T54), T55, X63)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → U4_GGAAGGA(T23, T24, T13, T14, T29, sameleavesC_in_gg(T24, T29))
U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → SAMELEAVESC_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U5_GGAAGGA(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → PB_IN_GGAAGGA(T70, tree(T71, T72), X89, X90, T13, T14, X17)
sameleavesC_in_gg(leaf(T6), leaf(T6)) → sameleavesC_out_gg(leaf(T6), leaf(T6))
sameleavesC_in_gg(tree(T11, T12), tree(T13, T14)) → U6_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_in_ggga(T13, T14, T23, X17))
getleaveA_in_ggga(leaf(T42), T43, T42, T43) → getleaveA_out_ggga(leaf(T42), T43, T42, T43)
getleaveA_in_ggga(tree(T52, T53), T54, T55, X63) → U1_ggga(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
U1_ggga(T52, T53, T54, T55, X63, getleaveA_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveA_out_ggga(tree(T52, T53), T54, T55, X63)
U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_out_ggga(T13, T14, T23, X17)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_in_gg(T24, T29))
U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_out_gg(T24, T29)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U6_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesC_out_gg(tree(T11, T12), tree(T13, T14))
SAMELEAVESC_IN_GG(tree(T11, T12), tree(T13, T14)) → U6_GG(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
SAMELEAVESC_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, X15, X16, T13, T14, X17)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → U2_GGAAGGA(T23, T24, T13, T14, X17, getleaveA_in_ggga(T13, T14, T23, X17))
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, X17) → GETLEAVEA_IN_GGGA(T13, T14, T23, X17)
GETLEAVEA_IN_GGGA(tree(T52, T53), T54, T55, X63) → U1_GGGA(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
GETLEAVEA_IN_GGGA(tree(T52, T53), T54, T55, X63) → GETLEAVEA_IN_GGGA(T52, tree(T53, T54), T55, X63)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → U4_GGAAGGA(T23, T24, T13, T14, T29, sameleavesC_in_gg(T24, T29))
U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → SAMELEAVESC_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U5_GGAAGGA(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → PB_IN_GGAAGGA(T70, tree(T71, T72), X89, X90, T13, T14, X17)
sameleavesC_in_gg(leaf(T6), leaf(T6)) → sameleavesC_out_gg(leaf(T6), leaf(T6))
sameleavesC_in_gg(tree(T11, T12), tree(T13, T14)) → U6_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_in_ggga(T13, T14, T23, X17))
getleaveA_in_ggga(leaf(T42), T43, T42, T43) → getleaveA_out_ggga(leaf(T42), T43, T42, T43)
getleaveA_in_ggga(tree(T52, T53), T54, T55, X63) → U1_ggga(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
U1_ggga(T52, T53, T54, T55, X63, getleaveA_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveA_out_ggga(tree(T52, T53), T54, T55, X63)
U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_out_ggga(T13, T14, T23, X17)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_in_gg(T24, T29))
U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_out_gg(T24, T29)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U6_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesC_out_gg(tree(T11, T12), tree(T13, T14))
GETLEAVEA_IN_GGGA(tree(T52, T53), T54, T55, X63) → GETLEAVEA_IN_GGGA(T52, tree(T53, T54), T55, X63)
sameleavesC_in_gg(leaf(T6), leaf(T6)) → sameleavesC_out_gg(leaf(T6), leaf(T6))
sameleavesC_in_gg(tree(T11, T12), tree(T13, T14)) → U6_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_in_ggga(T13, T14, T23, X17))
getleaveA_in_ggga(leaf(T42), T43, T42, T43) → getleaveA_out_ggga(leaf(T42), T43, T42, T43)
getleaveA_in_ggga(tree(T52, T53), T54, T55, X63) → U1_ggga(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
U1_ggga(T52, T53, T54, T55, X63, getleaveA_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveA_out_ggga(tree(T52, T53), T54, T55, X63)
U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_out_ggga(T13, T14, T23, X17)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_in_gg(T24, T29))
U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_out_gg(T24, T29)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U6_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesC_out_gg(tree(T11, T12), tree(T13, T14))
GETLEAVEA_IN_GGGA(tree(T52, T53), T54, T55, X63) → GETLEAVEA_IN_GGGA(T52, tree(T53, T54), T55, X63)
GETLEAVEA_IN_GGGA(tree(T52, T53), T54, T55) → GETLEAVEA_IN_GGGA(T52, tree(T53, T54), T55)
From the DPs we obtained the following set of size-change graphs:
SAMELEAVESC_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, X15, X16, T13, T14, X17)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → SAMELEAVESC_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → PB_IN_GGAAGGA(T70, tree(T71, T72), X89, X90, T13, T14, X17)
sameleavesC_in_gg(leaf(T6), leaf(T6)) → sameleavesC_out_gg(leaf(T6), leaf(T6))
sameleavesC_in_gg(tree(T11, T12), tree(T13, T14)) → U6_gg(T11, T12, T13, T14, pB_in_ggaagga(T11, T12, X15, X16, T13, T14, X17))
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17) → U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_in_ggga(T13, T14, T23, X17))
getleaveA_in_ggga(leaf(T42), T43, T42, T43) → getleaveA_out_ggga(leaf(T42), T43, T42, T43)
getleaveA_in_ggga(tree(T52, T53), T54, T55, X63) → U1_ggga(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
U1_ggga(T52, T53, T54, T55, X63, getleaveA_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveA_out_ggga(tree(T52, T53), T54, T55, X63)
U2_ggaagga(T23, T24, T13, T14, X17, getleaveA_out_ggga(T13, T14, T23, X17)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, X17)
pB_in_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_ggaagga(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_in_gg(T24, T29))
U4_ggaagga(T23, T24, T13, T14, T29, sameleavesC_out_gg(T24, T29)) → pB_out_ggaagga(leaf(T23), T24, T23, T24, T13, T14, T29)
pB_in_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17) → U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_in_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17))
U5_ggaagga(T70, T71, T72, X89, X90, T13, T14, X17, pB_out_ggaagga(T70, tree(T71, T72), X89, X90, T13, T14, X17)) → pB_out_ggaagga(tree(T70, T71), T72, X89, X90, T13, T14, X17)
U6_gg(T11, T12, T13, T14, pB_out_ggaagga(T11, T12, X15, X16, T13, T14, X17)) → sameleavesC_out_gg(tree(T11, T12), tree(T13, T14))
SAMELEAVESC_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, X15, X16, T13, T14, X17)
PB_IN_GGAAGGA(leaf(T23), T24, T23, T24, T13, T14, T29) → U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_in_ggga(T13, T14, T23, T29))
U3_GGAAGGA(T23, T24, T13, T14, T29, getleaveA_out_ggga(T13, T14, T23, T29)) → SAMELEAVESC_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, X89, X90, T13, T14, X17) → PB_IN_GGAAGGA(T70, tree(T71, T72), X89, X90, T13, T14, X17)
getleaveA_in_ggga(leaf(T42), T43, T42, T43) → getleaveA_out_ggga(leaf(T42), T43, T42, T43)
getleaveA_in_ggga(tree(T52, T53), T54, T55, X63) → U1_ggga(T52, T53, T54, T55, X63, getleaveA_in_ggga(T52, tree(T53, T54), T55, X63))
U1_ggga(T52, T53, T54, T55, X63, getleaveA_out_ggga(T52, tree(T53, T54), T55, X63)) → getleaveA_out_ggga(tree(T52, T53), T54, T55, X63)
SAMELEAVESC_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, T13, T14)
PB_IN_GGAAGGA(leaf(T23), T24, T13, T14) → U3_GGAAGGA(T23, T24, getleaveA_in_ggga(T13, T14, T23))
U3_GGAAGGA(T23, T24, getleaveA_out_ggga(T29)) → SAMELEAVESC_IN_GG(T24, T29)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
getleaveA_in_ggga(leaf(T42), T43, T42) → getleaveA_out_ggga(T43)
getleaveA_in_ggga(tree(T52, T53), T54, T55) → U1_ggga(getleaveA_in_ggga(T52, tree(T53, T54), T55))
U1_ggga(getleaveA_out_ggga(X63)) → getleaveA_out_ggga(X63)
getleaveA_in_ggga(x0, x1, x2)
U1_ggga(x0)
The following rules are removed from R:
PB_IN_GGAAGGA(leaf(T23), T24, T13, T14) → U3_GGAAGGA(T23, T24, getleaveA_in_ggga(T13, T14, T23))
U3_GGAAGGA(T23, T24, getleaveA_out_ggga(T29)) → SAMELEAVESC_IN_GG(T24, T29)
Used ordering: POLO with Polynomial interpretation [POLO]:
getleaveA_in_ggga(leaf(T42), T43, T42) → getleaveA_out_ggga(T43)
POL(PB_IN_GGAAGGA(x1, x2, x3, x4)) = 2·x1 + 2·x2 + 2·x3 + 2·x4
POL(SAMELEAVESC_IN_GG(x1, x2)) = 2·x1 + 2·x2
POL(U1_ggga(x1)) = x1
POL(U3_GGAAGGA(x1, x2, x3)) = 1 + x1 + 2·x2 + x3
POL(getleaveA_in_ggga(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(getleaveA_out_ggga(x1)) = 2·x1
POL(leaf(x1)) = 2 + 2·x1
POL(tree(x1, x2)) = x1 + x2
SAMELEAVESC_IN_GG(tree(T11, T12), tree(T13, T14)) → PB_IN_GGAAGGA(T11, T12, T13, T14)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
getleaveA_in_ggga(tree(T52, T53), T54, T55) → U1_ggga(getleaveA_in_ggga(T52, tree(T53, T54), T55))
U1_ggga(getleaveA_out_ggga(X63)) → getleaveA_out_ggga(X63)
getleaveA_in_ggga(x0, x1, x2)
U1_ggga(x0)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
getleaveA_in_ggga(tree(T52, T53), T54, T55) → U1_ggga(getleaveA_in_ggga(T52, tree(T53, T54), T55))
U1_ggga(getleaveA_out_ggga(X63)) → getleaveA_out_ggga(X63)
getleaveA_in_ggga(x0, x1, x2)
U1_ggga(x0)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
getleaveA_in_ggga(x0, x1, x2)
U1_ggga(x0)
getleaveA_in_ggga(x0, x1, x2)
U1_ggga(x0)
PB_IN_GGAAGGA(tree(T70, T71), T72, T13, T14) → PB_IN_GGAAGGA(T70, tree(T71, T72), T13, T14)
From the DPs we obtained the following set of size-change graphs: